D:Dsys, discrete:(IdId).
Feasible(D)
 d-feasible-discrete(D;discrete)
 (w:World. (PossibleWorld(D;w) & (i, x:Id. discrete(i;x) = discrete(i,x)))) 

latex

Definitions	t  T, P  Q, x:A. B(x), M.ds(x), z != f(x)  P(a;z), t.2, t.1, f(x)?z, M.ef(k,x,s,v)?w, shift-state(s), M.ef(k,x,s,v,w), ff, tt, read-state(s), if b then t else f fi , b, x. t(x), True, M.da(a), suptype(S; T), S  T, , Top, Valtype(da;k), M.(timed)state, MsgA, False, Unit, , x(s), P & Q, Feasible(D), P  Q,
Lemmas	msga wf, d-m wf, ma-tst wf, Knd wf, d-decl wf, d-feasible wf, false wf, true wf, bool wf, fpf-dom wf, read-state wf2, assert wf, fpf-ap wf, IdLnk wf, d-decl-subtype, ma-da wf, top wf, fpf-cap wf, subtype rel self, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, rationals wf, eqtt to assert, Id wf, fpf-trivial-subtype-top, int inc rationals, qsub wf, qadd wf